↳ Prolog
↳ PrologToPiTRSProof
flatten_in(cons(cons(U, V), W), X) → U2(U, V, W, X, flatten_in(cons(U, cons(V, W)), X))
flatten_in(cons(atom(X), U), .(X, Y)) → U1(X, U, Y, flatten_in(U, Y))
flatten_in(atom(X), .(X, [])) → flatten_out(atom(X), .(X, []))
U1(X, U, Y, flatten_out(U, Y)) → flatten_out(cons(atom(X), U), .(X, Y))
U2(U, V, W, X, flatten_out(cons(U, cons(V, W)), X)) → flatten_out(cons(cons(U, V), W), X)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
flatten_in(cons(cons(U, V), W), X) → U2(U, V, W, X, flatten_in(cons(U, cons(V, W)), X))
flatten_in(cons(atom(X), U), .(X, Y)) → U1(X, U, Y, flatten_in(U, Y))
flatten_in(atom(X), .(X, [])) → flatten_out(atom(X), .(X, []))
U1(X, U, Y, flatten_out(U, Y)) → flatten_out(cons(atom(X), U), .(X, Y))
U2(U, V, W, X, flatten_out(cons(U, cons(V, W)), X)) → flatten_out(cons(cons(U, V), W), X)
FLATTEN_IN(cons(cons(U, V), W), X) → U21(U, V, W, X, flatten_in(cons(U, cons(V, W)), X))
FLATTEN_IN(cons(cons(U, V), W), X) → FLATTEN_IN(cons(U, cons(V, W)), X)
FLATTEN_IN(cons(atom(X), U), .(X, Y)) → U11(X, U, Y, flatten_in(U, Y))
FLATTEN_IN(cons(atom(X), U), .(X, Y)) → FLATTEN_IN(U, Y)
flatten_in(cons(cons(U, V), W), X) → U2(U, V, W, X, flatten_in(cons(U, cons(V, W)), X))
flatten_in(cons(atom(X), U), .(X, Y)) → U1(X, U, Y, flatten_in(U, Y))
flatten_in(atom(X), .(X, [])) → flatten_out(atom(X), .(X, []))
U1(X, U, Y, flatten_out(U, Y)) → flatten_out(cons(atom(X), U), .(X, Y))
U2(U, V, W, X, flatten_out(cons(U, cons(V, W)), X)) → flatten_out(cons(cons(U, V), W), X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
FLATTEN_IN(cons(cons(U, V), W), X) → U21(U, V, W, X, flatten_in(cons(U, cons(V, W)), X))
FLATTEN_IN(cons(cons(U, V), W), X) → FLATTEN_IN(cons(U, cons(V, W)), X)
FLATTEN_IN(cons(atom(X), U), .(X, Y)) → U11(X, U, Y, flatten_in(U, Y))
FLATTEN_IN(cons(atom(X), U), .(X, Y)) → FLATTEN_IN(U, Y)
flatten_in(cons(cons(U, V), W), X) → U2(U, V, W, X, flatten_in(cons(U, cons(V, W)), X))
flatten_in(cons(atom(X), U), .(X, Y)) → U1(X, U, Y, flatten_in(U, Y))
flatten_in(atom(X), .(X, [])) → flatten_out(atom(X), .(X, []))
U1(X, U, Y, flatten_out(U, Y)) → flatten_out(cons(atom(X), U), .(X, Y))
U2(U, V, W, X, flatten_out(cons(U, cons(V, W)), X)) → flatten_out(cons(cons(U, V), W), X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
FLATTEN_IN(cons(atom(X), U), .(X, Y)) → FLATTEN_IN(U, Y)
FLATTEN_IN(cons(cons(U, V), W), X) → FLATTEN_IN(cons(U, cons(V, W)), X)
flatten_in(cons(cons(U, V), W), X) → U2(U, V, W, X, flatten_in(cons(U, cons(V, W)), X))
flatten_in(cons(atom(X), U), .(X, Y)) → U1(X, U, Y, flatten_in(U, Y))
flatten_in(atom(X), .(X, [])) → flatten_out(atom(X), .(X, []))
U1(X, U, Y, flatten_out(U, Y)) → flatten_out(cons(atom(X), U), .(X, Y))
U2(U, V, W, X, flatten_out(cons(U, cons(V, W)), X)) → flatten_out(cons(cons(U, V), W), X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
FLATTEN_IN(cons(atom(X), U), .(X, Y)) → FLATTEN_IN(U, Y)
FLATTEN_IN(cons(cons(U, V), W), X) → FLATTEN_IN(cons(U, cons(V, W)), X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ UsableRulesReductionPairsProof
FLATTEN_IN(cons(cons(U, V), W)) → FLATTEN_IN(cons(U, cons(V, W)))
FLATTEN_IN(cons(atom(X), U)) → FLATTEN_IN(U)
No rules are removed from R.
FLATTEN_IN(cons(cons(U, V), W)) → FLATTEN_IN(cons(U, cons(V, W)))
FLATTEN_IN(cons(atom(X), U)) → FLATTEN_IN(U)
POL(FLATTEN_IN(x1)) = 2·x1
POL(atom(x1)) = x1
POL(cons(x1, x2)) = 2 + 2·x1 + x2
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ PisEmptyProof